open structures

-- CIC


sig FullFledgedEA {
	ea: one EA,
	portSignatures: EAP set -> lone S,
	subElements: EASE lone -> lone FullFledgedEA,
	node: one ND,
	features: FT set -> lone FV,
	attributes: AT set -> lone AV
}

pred isSubElement[parent: FullFledgedEA, child: FullFledgedEA] {
    child in parent.subElements[univ]
}
fact FullFledgedEAHierarchyIsTree  {
	// There are no cycles among element instances
	no iden & ^{source: FullFledgedEA, target: FullFledgedEA | isSubElement[source, target] }

	// Every element instance has exactly one owner
	all inst: FullFledgedEA | not inst in CIC.rmap[univ].unit <=> one owner: FullFledgedEA | isSubElement[owner, inst] 
}

sig DRURMapping {
	unit: one FullFledgedEA,
	signature: one S,
	role: one CSR,
}

one sig CIC {
	// Partial connector architecture chosen by the resolver
	ca: one CA,
	
	rmap: DRDR one -> lone DRURMapping,
	
	features: FT set -> lone FV
}

sig SBEntry {
	signature: one S,
	responsibleInstance: one FullFledgedEA,
	responsibleInstancePort: one EAPR
} {
	// (C) The entry is exclusively owned by SB
	one sb: SB | this in sb.entries

	// (V) The instance responsible for the entry must have the signature containing the entry as the signature for the specified port
	responsibleInstance.portSignatures[responsibleInstancePort] = entries.this
}

sig SB extends S {
	entries: set SBEntry
}
